i:Id, da:k:Knd fp Type, snd1, snd2:kl::Knd  IdLnk fp (:Id  Top) List.
snd1 || snd2
 (msg-spec-loc-decl(snd1  snd2;i;da)
  (msg-spec-loc-decl(snd1;i;da) & msg-spec-loc-decl(snd2;i;da))) 

latex

Definitions

, a  b, msg-spec-loc-decl(snd;i;da), s = t, source(l), map(f;as), f || g, if b then t else f fi , case b of inl(x) => s(x) | inr(y) => t(y), f  g, P  Q, P & Q, P  Q, left + right, P  Q, {T}, t.1, f(x), type List, product-deq(A;B;a;b), IdLnk, IdLnkDeq, <a, b>, , x  dom(f), KindDeq, rcv(l,tg), a:A fp B(a), x. t(x), x.A(x), Type, Knd, xL. P(x), P  Q, b, (x  l), x:AB(x), x:A. B(x), x:A  B(x), Id, t  T, Top, x:A.B(x), Void, Unit, , b, A, False, [], [car / cdr], #$n, t.2, Atom$n, s ~ t, SQType(T), , , A  B, a < b, i  j , ||as||, {x:A| B(x)}

Lemmas

bool sq, bool cases, member wf, length wf1, non neg length, nat wf, Id sq, pi2 wf, cons one one, le wf, not wf, bnot wf, bool wf, assert of bnot, eqff to assert, iff transitivity, eqtt to assert, fpf-join-ap-sq, l member wf, top wf, Id wf, Knd wf, fpf-trivial-subtype-top, rcv wf, Kind-deq wf, fpf-dom wf, assert wf, idlnk-deq wf, IdLnk wf, product-deq wf, fpf-ap wf, pi1 wf, fpf-join-dom, fpf-join wf, l all map, fpf wf, fpf-compatible wf, map wf, l all wf, lsrc wf